package ca.shojaei.mini_sat;

import java.util.Vector;

public class ForAllNext extends Clause {
	
	public ForAllNext() {
		super();
		this.unary = true;
		this.evaluable = true;
	}
	private Clause F;
	private String symbol = "a@";
	public ForAllNext(Clause f, String symbol) {
		super();
		F = f;
		this.symbol = symbol;
		this.unary = true;
	}
	
	public Clause getLeft(){
		return getF();
	}
	public void setLeft(Clause c){
		setF(c);
	}
	
	public Clause getRight(){
		return null;
	}
	public void setRight( Clause c){
		;
	}
	
	public Clause getF() {
		return F;
	}
	public void setF(Clause f) {
		F = f;
	}
	public String getSymbol() {
		if(this.negated){
			String str = "!".concat(this.symbol);
			return str;
		}
		return symbol;
	}
	public void setSymbol(String symbol) {
		this.symbol = symbol;
	}
	@Override
	public Vector<int[]> getDIMACS(Model m) {
		
		State cur = m.getCurrentStat();
		
		Vector<State> nexts = cur.getNexts();
		Vector<int []> exp = new Vector<int[]>();
		Vector<int []> pex = new Vector<int[]>();
		pex = this.F.getDIMACS(m);
		
		exp = and(pex,nexts.get(0).getAndVariables());
		for(int i = 1; i < nexts.size(); i++)
		{
			Vector<int[]> temp = and(pex,nexts.get(i).getAndVariables());
			
			exp = and(exp, temp);
		}
		
		//SAT.clean(exp);
		SAT.printVec(exp);
		
		return exp;
		
	}
	@Override
	public boolean evaluate(Model m) {

		boolean out = true;
		State cur = m.getCurrentStat();
		Vector<State> nexts = cur.getNexts();
		
		for(int i = 0; i < nexts.size(); i++)
		{
			m.setCurrentStat(nexts.get(i).getStateName());
			if(!F.evaluate(m))
			{
				m.setCurrentStat(cur.getStateName());
				out = false;
				break;
			}
		}
		
		if(this.negated)
			out = !out;
		
		return out;
		
	}
	
	

}
